$\forall$$T$:Type, $X$:MaInterface($T$), ${\it es}$:ES, $e$:E.
\\[0ex]($\uparrow$ma{-}in{-}interface(${\it es}$;$X$;$e$))
\\[0ex]$\Leftarrow\!\Rightarrow$ ((loc($e$) $\in$ ma{-}interface{-}locs($X$)) \& (kind($e$) $\in$ ma{-}interface{-}dom($X$;loc($e$))))